#ifndef _INSTRUMENTATION_H_
#define _INSTRUMENTATION_H_

#include <stdlib.h>
#include <wdm.h>
#include "storm.h"

#define TRUE 1
#define FALSE 0
#define UNLOCKED 0


// WDM
int cancelLockStatus;

// WDF
int hrequest, created_hrequest, hrctx, created_hrctx;
int htimer, htctx;
int hqueue, hqctx;
int hdevice, hdctx;
int hdriver;
int notused_4hfileobj;
int hbuffer;

#define COMPLETED_CHECK(Request) { \
  if (storm_nondet()) { \
    __hv_assume(__resource("COMPLETED", Request) == TRUE); \
    STORM_ASSERT(0 != 0); \
  } \
}

#define __preserve_instrumented \
__loop_assert(cancelLockStatus == __old(cancelLockStatus))

#define __preserve_all __preserve_globals __preserve_instrumented

#endif

